/-
Copyright (c) 2025 Antoine Chambert-Loir and Filippo Nuccio. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández, Filippo A. E. Nuccio
-/
module

public import Mathlib.Algebra.Group.Subgroup.Pointwise
public import Mathlib.Algebra.GroupWithZero.Submonoid.Instances
public import Mathlib.Algebra.GroupWithZero.WithZero

/-! # The range of a MonoidWithZeroHom
Given a `MonoidWithZeroHom` `f : A → B` whose codomain `B` is a `MonoidWithZero`, we define the
type `MonoidWithZeroHom.valueMonoid` as the submonoid of `Bˣ` generated by the invertible elements
in the range of `f`. For example, if `A = ℕ`, `f` is the natural cast to `B` where `B` is
* `ℝ≥0`, then `MonoidWithZero.valueMonoid` are the positive natural numbers in `ℝ≥0`;
* `WithZero ℤ`, then `MonoidWithZero.valueMonoid = {1}`.

`MonoidWithZeroHom.ValueMonoid₀` is the `MonoidWithZero` obtained by
adjoining `0` to the previous type.

Likewise, `MonoidWithZeroHom.valueGroup` is the *subgroup* of `Bˣ` generated by the invertible
elements in `range f` and `MonoidWithZeroHom.ValueGroup₀` adds a `0` to the previous group.

When `B` is commutative, then both `MonoidWithZeroHom.valueGroup f` and
`MonoidWithZeroHom.ValueGroup₀ f` are also commutative and the former can be described more
explicitly (see `MonoidWithZeroHom.mem_valueGroup_iff_of_comm`).

## Main declarations

* `valueMonoid f` is the smallest submonoid of `Bˣ` containing the range of `f`;
* `ValueMonoid₀ f` is the smallest monoid with `0` containing the range of `f`;
* `valueGroup f` is the smallest subgroup of `Bˣ` containing the range of `f`;
* `ValueMonoid₀ f` is the smallest group with `0` containing the range of `f`;
* When `B` is a group with zero, rather than merely a monoid with zero, the above definitions
  all coincide: see `valueMonoid_eq_valueGroup` for an equality as submonoids and
  `valueMonoid_eq_valueGroup'` for an equality as subsets.
* When `B` is a *commutative* group with zero, `MonoidWithZeroHom.valueGroup` can be
  explicitly described as the elements that are ratios of terms in `range f`, see
  `MonoidWithZeroHom.mem_valueGroup_iff_of_comm`.

## Implementation details
`MonoidWithZeroHom.valueMonoid` is defined explicitly in terms of its carrier, by proving the
required properties; that it coincides with the submonoid generated by the closure is proven in
`MonoidWithZeroHom.valueMonoid_eq_closure`, but using the latter as definition yields to unwanted
unfolding.
-/

@[expose] public section

namespace MonoidWithZeroHom

open Set Subgroup Submonoid

section mrange

variable {G H : Type*} [MulZeroOneClass G] [MulZeroOneClass H] [Nontrivial H] (f : G →*₀ H)

lemma mrange_nontrivial :
    Nontrivial (MonoidHom.mrange f) :=
  ⟨1, 0, by simp [Subtype.ext_iff]⟩

lemma range_nontrivial :
    (Set.range f).Nontrivial :=
  Set.nontrivial_coe_sort.mp f.mrange_nontrivial

end mrange

variable {A B F : Type*} [FunLike F A B] (f : F)

section MonoidWithZero

variable [MonoidWithZero A] [MonoidWithZero B] [MonoidWithZeroHomClass F A B]

/-- For a morphism of monoids with zero `f`, this is a smallest submonoid of the invertible
elements in the codomain containing the range of `f`. -/
def valueMonoid : Submonoid Bˣ where
  carrier := (↑)⁻¹' (range f)
  mul_mem' hb hb' := by
    obtain ⟨y, hy⟩ := hb
    obtain ⟨y', hy'⟩ := hb'
    use y * y'
    rw [map_mul, hy, hy', Units.val_mul]
  one_mem' := ⟨1, by simp⟩

lemma one_mem_valueMonoid : 1 ∈ valueMonoid f := ⟨1, map_one ..⟩

lemma coe_one : (⟨(1 : Bˣ), one_mem_valueMonoid f⟩ : valueMonoid f) = 1 := rfl

lemma mem_valueMonoid_iff {b : Bˣ} : b ∈ valueMonoid f ↔ b ∈ (↑)⁻¹' (range f) := Iff.rfl

lemma valueMonoid_eq_closure : valueMonoid f = Submonoid.closure ((↑)⁻¹' (range f)) :=
  (valueMonoid f).closure_eq.symm

/-- For a morphism of monoids with zero `f`, this is the smallest subgroup of the invertible
elements in the codomain containing the range of `f`. -/
def valueGroup : Subgroup Bˣ := closure (valueMonoid f)

lemma valueGroup_def : valueGroup f = Subgroup.closure (valueMonoid f) := rfl

/-- For a morphism of monoids with zero `f`, this is the smallest submonoid with zero of the
codomain containing the range of `f`. -/
abbrev ValueMonoid₀ := WithZero (valueMonoid f)

@[deprecated (since := "2025-09-03")] alias valueMonoid₀ := ValueMonoid₀

/-- For a morphism of monoids with zero `f`, this is a smallest subgroup with zero of the
codomain containing the range of `f`. -/
abbrev ValueGroup₀ := WithZero (valueGroup f)

@[deprecated (since := "2025-09-03")] alias valueGroup₀ := ValueGroup₀

lemma mem_valueMonoid {b : Bˣ} (hb : b.val ∈ range f) : b ∈ valueMonoid f := by
  tauto

lemma mem_valueGroup {b : Bˣ} (hb : b.1 ∈ range f) : b ∈ valueGroup f := by
  suffices b ∈ valueMonoid f from Subgroup.mem_closure.mpr fun _ a ↦ a this
  exact mem_valueMonoid _ hb

lemma inv_mem_valueGroup {b : Bˣ} (hb : b.1 ∈ range f) : b⁻¹ ∈ valueGroup f :=
  Subgroup.inv_mem _ (mem_valueGroup f hb)

end MonoidWithZero

noncomputable section GroupWithZero

variable [GroupWithZero A] [GroupWithZero B] [MonoidWithZeroHomClass F A B] {f}

/- When the *domain* is itself a group with zero, the `valueMonoid` and the `valueGroup` coincide.-/
lemma valueMonoid_eq_valueGroup : (valueMonoid f) = (valueGroup f).toSubmonoid := by
  rw [valueGroup_def, Subgroup.closure_toSubmonoid, Eq.comm]
  apply Submonoid.closure_eq_of_le
  · simp only [union_subset_iff, subset_refl, true_and]
    intro _ ⟨y, hy⟩
    use y⁻¹
    simp [hy]
  · simp [Submonoid.closure_union]

variable (f) in
lemma valueMonoid_eq_valueGroup' : (valueMonoid f : Set Bˣ) = valueGroup f := by
  rw [valueMonoid_eq_valueGroup, coe_toSubmonoid]

lemma valueGroup_eq_range : Units.val '' (valueGroup f) = (range f \ {0}) := by
  ext x
  simp only [mem_diff, mem_range, mem_singleton_iff, ← valueMonoid_eq_valueGroup' f, mem_image,
    SetLike.mem_coe, mem_valueMonoid_iff, mem_preimage, mem_range]
  constructor
  · rintro ⟨y, hy, rfl⟩
    simp only [Units.ne_zero, not_false_eq_true, and_true, hy]
  · rintro ⟨⟨y, hy⟩, hx₀⟩
    refine ⟨Units.mk0 x hx₀, ?_, rfl⟩
    simpa [Units.val_mk0, mem_range] using ⟨y, hy⟩

end GroupWithZero
section CommGroupWithZero
--
variable [MonoidWithZero A] [CommGroupWithZero B] [MonoidWithZeroHomClass F A B]

theorem mem_valueGroup_iff_of_comm {y : Bˣ} :
    y ∈ valueGroup f ↔ ∃ a, f a ≠ 0 ∧ ∃ x, f a * y = f x := by
  refine ⟨fun hy ↦ ?_, fun ⟨a, ha, x, hy⟩ ↦ ?_⟩
  · simp only [valueGroup, valueMonoid, Submonoid.coe_set_mk, Subsemigroup.coe_set_mk] at hy
    induction hy using Subgroup.closure_induction with
    | mem _ h =>
      obtain ⟨a, ha⟩ := h
      exact ⟨a, ha.symm ▸ Units.ne_zero _, ⟨a * a, by simp [← ha]⟩⟩
    | one => exact ⟨1, by simp, 1, by simp⟩
    | mul c d hc hd hcy hdy =>
      obtain ⟨u, hu, a, ha⟩ := hcy
      obtain ⟨v, hv, b, hb⟩ := hdy
      refine ⟨u * v, by simp [hu, hv], a * b, ?_⟩
      simpa [map_mul, Units.val_mul, ← hb, ← ha] using mul_mul_mul_comm ..
    | inv c hc hcy  =>
      obtain ⟨u, hu, a, ha⟩ := hcy
      exact ⟨a, by simp [← ha, hu], u, by simp [← ha]⟩
  · have hv : f x ≠ 0 := by
      simp only [← hy, ne_eq, mul_eq_zero, ha, Units.ne_zero, or_self, not_false_eq_true]
    let v := (Ne.isUnit hv).unit
    have hv₀ : f x = ↑v := IsUnit.unit_spec (Ne.isUnit hv)
    let u := (Ne.isUnit ha).unit
    have ha₀ : f a = ↑u := IsUnit.unit_spec (Ne.isUnit ha)
    rw_mod_cast [hv₀, ha₀, Eq.comm, ← inv_mul_eq_iff_eq_mul] at hy
    rw [← hy]
    apply Subgroup.mul_mem
    · apply inv_mem_valueGroup
      use a
    · apply mem_valueGroup
      use x

instance : CommGroupWithZero (ValueGroup₀ f) where

end CommGroupWithZero

end MonoidWithZeroHom

namespace MonoidHomWithZero

@[deprecated (since := "2025-07-02")] alias valueMonoid := MonoidWithZeroHom.valueMonoid
@[deprecated (since := "2025-07-02")] alias valueGroup := MonoidWithZeroHom.valueGroup
@[deprecated (since := "2025-07-02")] alias valueMonoid₀ := MonoidWithZeroHom.ValueMonoid₀
@[deprecated (since := "2025-07-02")] alias valueGroup₀ := MonoidWithZeroHom.ValueGroup₀

end MonoidHomWithZero
